| Definition sig_fst {A B} {p q : {x : A | B x}} (H : p = q) | |
| : proj1_sig p = proj1_sig q := | |
| eq_rect _ (fun z => proj1_sig p = proj1_sig z) eq_refl _ H. | |
| Definition sig_snd {A B} {p q : {x : A | B x}} (H : p = q) | |
| : eq_rect _ B (proj2_sig p) _ (sig_fst H) = proj2_sig q := | |
| match H with | |
| | eq_refl => eq_refl | |
| end. |
This post intends to promote self types as a safer, simpler, and faster alternative to inductive types and dependent pattern matching at the core of programming languages.
In summary, it should go through the problems that self types try to solve, the problems that they introduce, and then a concrete solution proposed at the end, with a syntax-directed, bidirectional type system with decidable checking.
SYNTAX at the Syntax section.
| name | bikeshed |
|---|---|
| description | Run two independent subagents through a structured debate on the same prompt — independent answers, cross-critique, revision, then a synthesized unified response. Use when explicitly invoked as /bikeshed with a prompt, or when the user asks for a two-agent debate/adversarial comparison on a plan, design, or other complex piece of work. Best for plans and complex open-ended work, not simple factual questions. |
Take the user's prompt (everything after /bikeshed), run it through two independent subagents in a debate protocol, and synthesize their final answers into one unified response. If no prompt was given, ask the user what question or plan to bikeshed before starting.
The value comes from independence followed by controlled exchange. Do not let either agent see the other's work before Round 1 is complete, and do not editorialize when relaying material between them — pass responses and critiques verbatim.
GLM-5.2 is Z.ai's open-weights (MIT) flagship — 744B-MoE, a 1M-token context, and benchmarks within ~1 point of Claude Opus 4.8 on FrontierSWE. Here's how to actually put it to work, starting with the routes that cost nothing and need no credit card.
| #!/bin/bash | |
| TIMESTORE="/var/lib/avc-audit-report.last-run" | |
| TMPFILE=`mktemp /tmp/avc-audit-report.XXXXXXXXXX` | |
| if [ -e "$TIMESTORE" ]; then | |
| LASTRUN=`cat ${TIMESTORE}` | |
| else | |
| LASTRUN="yesterday" | |
| fi |
| #!/bin/bash | |
| WANT=$1 | |
| dotime () { | |
| WANT=$1 | |
| PAC=`TZ='America/Vancouver' date +%H:%M -d "TZ=\"America/Montreal\" $WANT"` | |
| MTN=`TZ='America/Denver' date +%H:%M -d "TZ=\"America/Montreal\" $WANT"` | |
| CEN=`TZ='America/Chicago' date +%H:%M -d "TZ=\"America/Montreal\" $WANT"` | |
| UTC=`TZ='Etc/UTC' date +%H:%M -d "TZ=\"America/Montreal\" $WANT"` | |
| CST=`TZ='Asia/Shanghai' date +%H:%M -d "TZ=\"America/Montreal\" $WANT"` |
| #!/bin/bash | |
| SNAPLOCK="/mnt/snaplock" | |
| for ZONE in internal dmz frontend; do | |
| YESTERDAY=`date +'%Y/%m/%d' -d 'yesterday'` | |
| TOMORROW=`date +'%Y/%m/%d' -d 'tomorrow'` | |
| LOCKTILL=`date +'%Y%m%d0000' -d '+5 years'` | |
| if [ -d "${SNAPLOCK}/${ZONE}/${YESTERDAY}" ]; then |
| module mysnaplock 1.0.0; | |
| require { | |
| type cron_log_t; | |
| type var_log_t; | |
| class filesystem associate; | |
| } | |
| #============= cron_log_t ============== | |
| allow cron_log_t var_log_t:filesystem associate; |
| #!/bin/bash | |
| # Downtimes are third Sunday of the month. In order to plan | |
| # for upgrades and reboots, we email ourselves the list of all | |
| # outstanding security updates for each system on the 2nd | |
| # Wednesday of the month. | |
| # Critical security update alerts are sent daily. | |
| # Requires yum-plugin-security and mailx. | |
| WEEKOFMONTH=$((($(date +%d)-1)/7+1)) | |
| DAYOFWEEK=$(date +%u) |
I hereby claim:
To claim this, I am signing this object: